Left Termination of the query pattern
flat(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

right(tree(X, XS1, XS2), XS2).
flat(niltree, nil).
flat(tree(X, niltree, XS), cons(X, YS)) :- ','(right(tree(X, niltree, XS), ZS), flat(ZS, YS)).
flat(tree(X, tree(Y, YS1, YS2), XS), ZS) :- flat(tree(Y, YS1, tree(X, YS2, XS)), ZS).

Query: flat(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: flat(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: flat(T1, T2), SCOPE: 1, CLAUSE: 1 | flat(T1, T2), SCOPE: 1, CLAUSE: 2 | flat(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | flat(niltree, T2), SCOPE: 1, CLAUSE: 2 | flat(niltree, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: flat(T1, T2), SCOPE: 1, CLAUSE: 2 | flat(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nflat(T1, T2) !=? flat(niltree, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: flat(niltree, T2), SCOPE: 1, CLAUSE: 2 | flat(niltree, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: flat(niltree, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(right(tree(T6, niltree, T7), X16), flat(X16, T9)) | flat(tree(T6, niltree, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: flat(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nX13 is free\nX14 is free\nX15 is free\nflat(T1, T2) !=? flat(niltree, nil)\nflat(T1, T2) !=? flat(tree(X13, niltree, X14), cons(X13, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(right(tree(T6, niltree, T7), X16), flat(X16, T9)), SCOPE: 2, CLAUSE: 0 | ?_2 | flat(tree(T6, niltree, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(right(tree(T6, niltree, T7), X16), flat(X16, T9)), SCOPE: 2, CLAUSE: 0\n\nT6 is ground\nT7 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ?_2 | flat(tree(T6, niltree, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: flat(T19, T9)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: flat(tree(T6, niltree, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: flat(tree(T28, T29, tree(T27, T30, T31)), T33)\n\nT27 is ground\nT28 is ground\nT29 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 1 | flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 2 | flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 3\n\nT27 is ground\nT28 is ground\nT29 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 2 | flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 3\n\nT27 is ground\nT28 is ground\nT29 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 2\n\nT27 is ground\nT28 is ground\nT29 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: flat(tree(T28, T29, tree(T27, T30, T31)), T33), SCOPE: 3, CLAUSE: 3\n\nT27 is ground\nT28 is ground\nT29 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(right(tree(T54, niltree, tree(T55, T56, T57)), X67), flat(X67, T59))\n\nT54 is ground\nT55 is ground\nT56 is ground\nT57 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(right(tree(T54, niltree, tree(T55, T56, T57)), X67), flat(X67, T59)), SCOPE: 4, CLAUSE: 0\n\nT54 is ground\nT55 is ground\nT56 is ground\nT57 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: flat(tree(T69, T70, T71), T59)\n\nT69 is ground\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: flat(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)\n\nT88 is ground\nT89 is ground\nT90 is ground\nT91 is ground\nT92 is ground\nT93 is ground\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 28 [arrowhead = none ];
28 -> 2;

29 [label="EVAL with clause\nflat(niltree, nil).\nand substitutionT1 -> niltree,\nT2 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 29 [arrowhead = none ];
29 -> 3;

30 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 30 [arrowhead = none ];
30 -> 4;

31 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 31 [arrowhead = none ];
31 -> 5;

32 [label="EVAL with clause\nflat(tree(X13, niltree, X14), cons(X13, X15)) :- ','(right(tree(X13, niltree, X14), X16), flat(X16, X15)).\nand substitutionX13 -> T6,\nX14 -> T7,\nT1 -> tree(T6, niltree, T7),\nX15 -> T9,\nT2 -> cons(T6, T9),\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 32 [arrowhead = none ];
32 -> 8;

33 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 33 [arrowhead = none ];
33 -> 9;

34 [label="BACKTRACK\nfor clause: flat(tree(X, niltree, XS), cons(X, YS)) :- ','(right(tree(X, niltree, XS), ZS), flat(ZS, YS))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 34 [arrowhead = none ];
34 -> 6;

35 [label="BACKTRACK\nfor clause: flat(tree(X, tree(Y, YS1, YS2), XS), ZS) :- flat(tree(Y, YS1, tree(X, YS2, XS)), ZS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 35 [arrowhead = none ];
35 -> 7;

36 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 36 [arrowhead = none ];
36 -> 10;

37 [label="EVAL with clause\nflat(tree(X44, tree(X45, X46, X47), X48), X49) :- flat(tree(X45, X46, tree(X44, X47, X48)), X49).\nand substitutionX44 -> T27,\nX45 -> T28,\nX46 -> T29,\nX47 -> T30,\nX48 -> T31,\nT1 -> tree(T27, tree(T28, T29, T30), T31),\nT2 -> T33,\nX49 -> T33,\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 37 [arrowhead = none ];
37 -> 16;

38 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 38 [arrowhead = none ];
38 -> 17;

39 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 39 [arrowhead = none ];
39 -> 11;

40 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 40 [arrowhead = none ];
40 -> 12;

41 [label="ONLY EVAL with clause\nright(tree(X29, X30, X31), X31).\nand substitutionT6 -> T18,\nX29 -> T18,\nX30 -> niltree,\nT7 -> T19,\nX31 -> T19,\nX16 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 41 [arrowhead = none ];
41 -> 13;

42 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 42 [arrowhead = none ];
42 -> 14;

43 [label="INSTANCE with matching:\nT1 -> T19\nT2 -> T9", fontsize=14, style = filled, fillcolor = lightgrey];
13 -> 43 [arrowhead = none , style=dashed];
43 -> 1[style=dashed];

44 [label="BACKTRACK\nfor clause: flat(tree(X, tree(Y, YS1, YS2), XS), ZS) :- flat(tree(Y, YS1, tree(X, YS2, XS)), ZS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 44 [arrowhead = none ];
44 -> 15;

45 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 45 [arrowhead = none ];
45 -> 18;

46 [label="BACKTRACK\nfor clause: flat(niltree, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 46 [arrowhead = none ];
46 -> 19;

47 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
19 -> 47 [arrowhead = none ];
47 -> 20;

48 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
19 -> 48 [arrowhead = none ];
48 -> 21;

49 [label="EVAL with clause\nflat(tree(X64, niltree, X65), cons(X64, X66)) :- ','(right(tree(X64, niltree, X65), X67), flat(X67, X66)).\nand substitutionT28 -> T54,\nX64 -> T54,\nT29 -> niltree,\nT27 -> T55,\nT30 -> T56,\nT31 -> T57,\nX65 -> tree(T55, T56, T57),\nX66 -> T59,\nT33 -> cons(T54, T59),\nT58 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 49 [arrowhead = none ];
49 -> 22;

50 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 50 [arrowhead = none ];
50 -> 23;

51 [label="EVAL with clause\nflat(tree(X89, tree(X90, X91, X92), X93), X94) :- flat(tree(X90, X91, tree(X89, X92, X93)), X94).\nand substitutionT28 -> T88,\nX89 -> T88,\nX90 -> T89,\nX91 -> T90,\nX92 -> T91,\nT29 -> tree(T89, T90, T91),\nT27 -> T92,\nT30 -> T93,\nT31 -> T94,\nX93 -> tree(T92, T93, T94),\nT33 -> T96,\nX94 -> T96,\nT95 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 51 [arrowhead = none ];
51 -> 26;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 52 [arrowhead = none ];
52 -> 27;

53 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 53 [arrowhead = none ];
53 -> 24;

54 [label="ONLY EVAL with clause\nright(tree(X74, X75, X76), X76).\nand substitutionT54 -> T68,\nX74 -> T68,\nX75 -> niltree,\nT55 -> T69,\nT56 -> T70,\nT57 -> T71,\nX76 -> tree(T69, T70, T71),\nX67 -> tree(T69, T70, T71)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 54 [arrowhead = none ];
54 -> 25;

55 [label="INSTANCE with matching:\nT1 -> tree(T69, T70, T71)\nT2 -> T59", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 55 [arrowhead = none , style=dashed];
55 -> 1[style=dashed];

56 [label="INSTANCE with matching:\nT1 -> tree(T89, T90, tree(T88, T91, tree(T92, T93, T94)))\nT2 -> T96", fontsize=14, style = filled, fillcolor = lightgrey];
26 -> 56 [arrowhead = none , style=dashed];
56 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

flatA(niltree, nil).
flatA(tree(T18, niltree, T19), cons(T18, T9)) :- flatA(T19, T9).
flatA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) :- flatA(tree(T69, T70, T71), T59).
flatA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) :- flatA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96).

Query: flatA(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
flatA_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

flatA_in_ga(niltree, nil) → flatA_out_ga(niltree, nil)
flatA_in_ga(tree(T18, niltree, T19), cons(T18, T9)) → U1_ga(T18, T19, T9, flatA_in_ga(T19, T9))
flatA_in_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_ga(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
flatA_in_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_out_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)) → flatA_out_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96)
U2_ga(T69, T68, T70, T71, T59, flatA_out_ga(tree(T69, T70, T71), T59)) → flatA_out_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59))
U1_ga(T18, T19, T9, flatA_out_ga(T19, T9)) → flatA_out_ga(tree(T18, niltree, T19), cons(T18, T9))

The argument filtering Pi contains the following mapping:
flatA_in_ga(x1, x2)  =  flatA_in_ga(x1)
niltree  =  niltree
flatA_out_ga(x1, x2)  =  flatA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_ga(x1, x2, x3, x4, x5, x6, x7, x9)
cons(x1, x2)  =  cons(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

flatA_in_ga(niltree, nil) → flatA_out_ga(niltree, nil)
flatA_in_ga(tree(T18, niltree, T19), cons(T18, T9)) → U1_ga(T18, T19, T9, flatA_in_ga(T19, T9))
flatA_in_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_ga(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
flatA_in_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_out_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)) → flatA_out_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96)
U2_ga(T69, T68, T70, T71, T59, flatA_out_ga(tree(T69, T70, T71), T59)) → flatA_out_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59))
U1_ga(T18, T19, T9, flatA_out_ga(T19, T9)) → flatA_out_ga(tree(T18, niltree, T19), cons(T18, T9))

The argument filtering Pi contains the following mapping:
flatA_in_ga(x1, x2)  =  flatA_in_ga(x1)
niltree  =  niltree
flatA_out_ga(x1, x2)  =  flatA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_ga(x1, x2, x3, x4, x5, x6, x7, x9)
cons(x1, x2)  =  cons(x1, x2)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → U1_GA(T18, T19, T9, flatA_in_ga(T19, T9))
FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → FLATA_IN_GA(T19, T9)
FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_GA(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → FLATA_IN_GA(tree(T69, T70, T71), T59)
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_GA(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)

The TRS R consists of the following rules:

flatA_in_ga(niltree, nil) → flatA_out_ga(niltree, nil)
flatA_in_ga(tree(T18, niltree, T19), cons(T18, T9)) → U1_ga(T18, T19, T9, flatA_in_ga(T19, T9))
flatA_in_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_ga(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
flatA_in_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_out_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)) → flatA_out_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96)
U2_ga(T69, T68, T70, T71, T59, flatA_out_ga(tree(T69, T70, T71), T59)) → flatA_out_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59))
U1_ga(T18, T19, T9, flatA_out_ga(T19, T9)) → flatA_out_ga(tree(T18, niltree, T19), cons(T18, T9))

The argument filtering Pi contains the following mapping:
flatA_in_ga(x1, x2)  =  flatA_in_ga(x1)
niltree  =  niltree
flatA_out_ga(x1, x2)  =  flatA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_ga(x1, x2, x3, x4, x5, x6, x7, x9)
cons(x1, x2)  =  cons(x1, x2)
FLATA_IN_GA(x1, x2)  =  FLATA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x1, x2, x3, x4, x6)
U3_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_GA(x1, x2, x3, x4, x5, x6, x7, x9)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → U1_GA(T18, T19, T9, flatA_in_ga(T19, T9))
FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → FLATA_IN_GA(T19, T9)
FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_GA(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → FLATA_IN_GA(tree(T69, T70, T71), T59)
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_GA(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)

The TRS R consists of the following rules:

flatA_in_ga(niltree, nil) → flatA_out_ga(niltree, nil)
flatA_in_ga(tree(T18, niltree, T19), cons(T18, T9)) → U1_ga(T18, T19, T9, flatA_in_ga(T19, T9))
flatA_in_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_ga(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
flatA_in_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_out_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)) → flatA_out_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96)
U2_ga(T69, T68, T70, T71, T59, flatA_out_ga(tree(T69, T70, T71), T59)) → flatA_out_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59))
U1_ga(T18, T19, T9, flatA_out_ga(T19, T9)) → flatA_out_ga(tree(T18, niltree, T19), cons(T18, T9))

The argument filtering Pi contains the following mapping:
flatA_in_ga(x1, x2)  =  flatA_in_ga(x1)
niltree  =  niltree
flatA_out_ga(x1, x2)  =  flatA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_ga(x1, x2, x3, x4, x5, x6, x7, x9)
cons(x1, x2)  =  cons(x1, x2)
FLATA_IN_GA(x1, x2)  =  FLATA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x1, x2, x3, x4, x6)
U3_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_GA(x1, x2, x3, x4, x5, x6, x7, x9)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → FLATA_IN_GA(tree(T69, T70, T71), T59)
FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → FLATA_IN_GA(T19, T9)
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)

The TRS R consists of the following rules:

flatA_in_ga(niltree, nil) → flatA_out_ga(niltree, nil)
flatA_in_ga(tree(T18, niltree, T19), cons(T18, T9)) → U1_ga(T18, T19, T9, flatA_in_ga(T19, T9))
flatA_in_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → U2_ga(T69, T68, T70, T71, T59, flatA_in_ga(tree(T69, T70, T71), T59))
flatA_in_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_in_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96))
U3_ga(T92, T88, T89, T90, T91, T93, T94, T96, flatA_out_ga(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)) → flatA_out_ga(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96)
U2_ga(T69, T68, T70, T71, T59, flatA_out_ga(tree(T69, T70, T71), T59)) → flatA_out_ga(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59))
U1_ga(T18, T19, T9, flatA_out_ga(T19, T9)) → flatA_out_ga(tree(T18, niltree, T19), cons(T18, T9))

The argument filtering Pi contains the following mapping:
flatA_in_ga(x1, x2)  =  flatA_in_ga(x1)
niltree  =  niltree
flatA_out_ga(x1, x2)  =  flatA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U3_ga(x1, x2, x3, x4, x5, x6, x7, x9)
cons(x1, x2)  =  cons(x1, x2)
FLATA_IN_GA(x1, x2)  =  FLATA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71), cons(T68, T59)) → FLATA_IN_GA(tree(T69, T70, T71), T59)
FLATA_IN_GA(tree(T18, niltree, T19), cons(T18, T9)) → FLATA_IN_GA(T19, T9)
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94), T96) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))), T96)

R is empty.
The argument filtering Pi contains the following mapping:
niltree  =  niltree
tree(x1, x2, x3)  =  tree(x1, x2, x3)
cons(x1, x2)  =  cons(x1, x2)
FLATA_IN_GA(x1, x2)  =  FLATA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71)) → FLATA_IN_GA(tree(T69, T70, T71))
FLATA_IN_GA(tree(T18, niltree, T19)) → FLATA_IN_GA(T19)
FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94)) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

FLATA_IN_GA(tree(T69, tree(T68, niltree, T70), T71)) → FLATA_IN_GA(tree(T69, T70, T71))
FLATA_IN_GA(tree(T18, niltree, T19)) → FLATA_IN_GA(T19)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(FLATA_IN_GA(x₁)) = 2·x₁   
POL(niltree) = 0   
POL(tree(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + x₃   

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94)) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FLATA_IN_GA(tree(T92, tree(T88, tree(T89, T90, T91), T93), T94)) → FLATA_IN_GA(tree(T89, T90, tree(T88, T91, tree(T92, T93, T94))))

Used ordering: Polynomial interpretation [POLO]:

POL(FLATA_IN_GA(x₁)) = 2·x₁   
POL(tree(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + x₃   

(16) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(17) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(18) YES